\begin{tabbing}
pre{-}init1{-}p(${\it es}$;$i$;$x$;$X$;$x_{0}$;$a$;$T$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\exists$$v$:$T$. $P$($x_{0}$,$v$)) $\Rightarrow$ ($\exists$$e$:es{-}E(${\it es}$). es{-}loc(${\it es}$; $e$) $=$ $i$ $\in$ Id))\+
\\[0ex]\& es{-}vartype(${\it es}$; $i$; $x$) $\subseteq\rho$ $X$
\\[0ex]\& \=alle{-}at(${\it es}$;$i$;$e$.\=es{-}kind(${\it es}$; $e$) $=$ locl($a$) $\in$ Knd\+\+
\\[0ex]$\Rightarrow$ es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ $T$ \& $P$(es{-}when(${\it es}$; $x$; $e$),es{-}val(${\it es}$; $e$)))
\-\\[0ex]\& \=alle{-}at(${\it es}$;$i$;$e$.existse{-}ge(${\it es}$;$e$;${\it e'}$.es{-}kind(${\it es}$; ${\it e'}$) $=$ locl($a$) $\in$ Knd\+
\\[0ex]$\vee$ ($\forall$$v$:$T$. $\neg$$P$(es{-}after(${\it es}$; $x$; ${\it e'}$),$v$))))
\-\-\\[0ex]\& init{-}p(${\it es}$; $i$; $X$; $x$; $x_{0}$)
\-
\end{tabbing}